--------------------------------------------------------------------------------
-- File: list_marquage_accessible.adb
--------------------------------------------------------------------------------

with Text_Io;

package body list_marquage_accessible is

   Package Io is new Text_Io.Integer_Io(Integer);
   type tabBoolean is array (1..maxTabMA) of boolean;


   ----------------------------------------------
   -- PROCEDURE Initialise
   -- Initialise la liste
   ----------------------------------------------
   procedure Initialise (listMarq : in out ListMarquage; indiceCourant : in out Integer; marqAcc : in marquage_accessible.MarquageAccessible) is
   begin
      --initialisation de l'indice courant à 1
      indiceCourant := 1;
      --ajout d'un Marquage Accessible au niveau de l'indice courant
      listMarq(indiceCourant) := marqAcc;
   end Initialise;


   ----------------------------------------------
   -- PROCEDURE add
   -- Ajoute a la tete de la liste
   ----------------------------------------------
   procedure add (listMarq : in out ListMarquage; indiceCourant : in out Integer; marquage : in marquage_accessible.Marquage; iterator : in Integer) is
      newMarqAcc : marquage_accessible.MarquageAccessible;
   begin
      --creation d'un nouveau Marquage Accessible et initialisation avec un Marquage
      marquage_accessible.create(newMarqAcc, marquage);
      --incrementation de l'indice courant de la liste
      indiceCourant := indiceCourant + 1 ;
      --insertion du nouveau Marquage Accessible dans la liste à l'indice courant
      listMarq(indiceCourant) := newMarqAcc ;
   end add;


   ----------------------------------------------
   -- PROCEDURE getTete
   -- Donne la tete de la liste
   ----------------------------------------------
   function getTete (listMarq : in ListMarquage; indiceCourant : in Integer) return marquage_accessible.Marquage is
   begin
      --retourne le marquage place au niveau de l'indice courant
      return listMarq(indiceCourant).M;
   end getTete;


   ----------------------------------------------
   -- PROCEDURE estFranchissable
   -- Test si le marquage est franchissable
   ----------------------------------------------
   function estFranchissable(iterator : in integer; marquage : in marquage_accessible.Marquage; matIM : in Matrices.matrice) return Boolean is
   begin
      --on parcours les places dans la matrice I-
      --iterator represente le numero de transition
      for i in 1.. marquage_accessible.nbPlace loop
         if( (matIM(i,iterator) > marquage(i)) AND (marquage(i) /= -1) ) then
            --si la valeur de I- pour une place(i) et une transition(iterator) est superieur
            --à la valeur du marquage pour une place i
            --on renvoit FALSE
            return false ;
         end if;
      end loop;
      --si aucun test n'est concluant, on en conclut que le marquage est franchissable
      --on renvoit TRUE
      return true ;
   end estFranchissable;


   ----------------------------------------------
   -- PROCEDURE contains
   -- Test si le marquage est dans la liste
   ----------------------------------------------
   function  contains  (listMarq : in ListMarquage; indiceCourant : in Integer; marquage : in marquage_accessible.Marquage) return Integer is
   begin
      --on parcours la liste de Marquage Accessible
      for i in 1 .. indiceCourant loop
         if(marquage_accessible.Egal(listMarq(i).M, marquage)) then
            --si un marquage de la liste correspond au marquage passe en parametre
            --on renvoit l'indice de la correspondance
            return i;
         end if;
      end loop;
      --sinon on renvoit -1
      return -1;
   end contains;


   ----------------------------------------------
   -- PROCEDURE containsMultiple
   -- Test si le marquage a un multiple dans la liste
   ----------------------------------------------
   procedure  containsMultiple  (listMarq : in ListMarquage; indiceCourant : in Integer; marquage : in out marquage_accessible.Marquage) is
   begin
      --on parcours la liste de Marquage Accessible
      for i in 1 .. indiceCourant loop
         if(marquage_accessible.SupEgal(marquage, listMarq(i).M)) then
            --si un marquage de la liste couvre le marquage passe en parametre
            --on le transforme en un marquage multiple
            marquage_accessible.BecomeMultiple (marquage, listMarq(i).M);
            return;
         end if;
      end loop;
   end containsMultiple;


   ----------------------------------------------
   -- PROCEDURE getFranchissement
   -- Renvoi le marquage genere par le franchissement
   ----------------------------------------------
   function  getFranchissement (iterator : in integer; marquage : in marquage_accessible.Marquage;matIM : in Matrices.matrice;matIP : in Matrices.matrice) return marquage_accessible.Marquage is
      newMarquage : marquage_accessible.Marquage;
   begin
      --on parcours la matrice I- (I- etant de même taille que I+, on utilise le meme indice)
      for i in 1 .. marquage_accessible.nbPlace loop
         --on creer un nouveau marquage si marquage(i) <> -1
         if (marquage(i) = -1)
         then
            newMarquage(i) := -1;
         else
            newMarquage(i) := marquage(i) + matIP(i,iterator) - matIM(i,iterator);
         end if;
      end loop;
      --retourne le nouveau marquage cree
      return newMarquage;
   end getFranchissement;


   ----------------------------------------------
   -- PROCEDURE addSuivant
   -- Ajoute une reference dans le tableau suivant
   ----------------------------------------------
   procedure addSuivant (listMarq : in out ListMarquage; indiceCourant : in Integer; indiceMarqSuiv : in Integer; indiceTransition : in Integer) is
   begin
      --ajoute dans le tableau de suivant à l'indice de la transition, l'indice du marquage suivant
      listMarq(indiceCourant).suivant(indiceTransition) := indiceMarqSuiv;
   end addSuivant;


   ----------------------------------------------
   -- PROCEDURE construire
   -- Algorithme de generation de Graphe de Marquage Accessible
   ----------------------------------------------
   procedure construire (listMarq : in out ListMarquage; indiceCourant : in out Integer; matIM : in Matrices.Matrice; matIP : in Matrices.Matrice) is
      --liste temporaire qui permet de stocker les marquages accessibles qui reste à traiter
      List_A_Explorer : ListMarquage;
      --variable temporaire pour le parcours de List_A_Explorer
      marqAccExp      : marquage_accessible.Marquage;
      --variable temporaire generee apres le franchissement
      marqAccGenerate : marquage_accessible.Marquage;
      --iterateur pour le parcours des transitions
      iterator        : Integer;
      --nombre de Transitions
      nbTransitions   : Integer := marquage_accessible.nbTransition;
      --indice courant pour la liste List_A_Explorer
      indiceCourantExp: Integer := 0;
      --variable temporaire. Stock le resultat de la verification lors du test si la transition est franchissable
      valPosition     : Integer := 0;
      --variable temporaire. Stocke l'indice du marquage suivant
      valMarqSuiv     : Integer := 0;
      --variable temporaire. Stocke l'indice de l'hypothetique marquage etant un multiple superieur
      valMarqMultSup      : Integer := 0;
   begin
      --on initialise List_A_Exploreret indiceCourantExp
      Initialise (List_A_Explorer, indiceCourantExp, listMarq(indiceCourant));

      --on parcours List_A_Explorer
      while (indiceCourantExp /= 0) loop
         --on recupere la tete de List_A_Explorer
         marqAccExp  := getTete(List_A_Explorer, indiceCourantExp) ;
         --on supprime la tete de List_A_Explorer
         indiceCourantExp := indiceCourantExp - 1;
         --on initialise l'iterateur a 1 (on se place sur la premiere transition)
         iterator := 1 ;
         --on parcours toutes les transitions de I-
         while (iterator <= nbTransitions)  loop
            --Si la transition est franchissable par marqAccExp
            if (estFranchissable(iterator, marqAccExp, matIM)) then
               --la transition est franchissable
               --on genere un nouveau marquage
               marqAccGenerate := getFranchissement(iterator, marqAccExp, matIM, matIP);
               --valPosition renvoit l'indice du nouveau marquage genere dans la liste principale (ou -1)
               valPosition := contains(listMarq, indiceCourant, marqAccGenerate);
               --on regarde si le marquage cree est multiple d'un marquage pre-existant
               containsMultiple(listMarq, indiceCourant, marqAccGenerate);
               --valPosition renvoit l'indice de marqAccExp dans la liste principale (ou -1)
               valMarqSuiv := contains(listMarq, indiceCourant, marqAccExp);

               if(valPosition = -1) then
                  --le nouveau marquage n'est pas present dans la liste principale
                  --on ajoute marqAccGenerate dans listMarq
                  add(listMarq, indiceCourant, marqAccGenerate, iterator);
                  --on ajoute marqAccGenerate dans list_A_Explorer
                  add(List_A_Explorer, indiceCourantExp, marqAccGenerate, iterator);
                  --on ajoute valMarqSuiv dans les suivant de listMarq à l'indiceCourant
                  addSuivant(listMarq, valMarqSuiv, indiceCourant, iterator);

               else
                  --le nouveau marquage est deja present dans la liste principale
                  --on ajoute valMarqSuiv dans les suivant de listMarq à l'indice de l'occurence
                  addSuivant(listMarq, valMarqSuiv, valPosition, iterator);
               end if;
            end if;
            --on incremente l'iterateur (on passe à la transition suivante)

            iterator := iterator + 1 ;
         end loop ;

      end loop ;
   end construire;


   ----------------------------------------------
   -- PROCEDURE estBorne
   -- Test si le reseau est borne
   ----------------------------------------------
   function    estBorne          (lMarq : in ListMarquage; nbCourant : in integer) return boolean is
   begin
      -- pour chaque marquage accessible
      for i in 1 .. nbCourant loop
         -- si tous les marquages sont <> de -1 (ie -1 <=> infini)
         -- alors le rdp est borne
         for j in 1 .. marquage_accessible.nbPlace loop
            if (lMarq(i).M(j) = -1)
            then return false;
            end if;
         end loop;
      end loop;
      return true;
   end estBorne;


   ----------------------------------------------
   -- PROCEDURE transitionEstVivante
   -- Test si une transition est vivante pour un marquage donne
   ----------------------------------------------
   procedure    transitionEstVivante  (lMarq : in ListMarquage; marq : in marquage_accessible.MarquageAccessible; transition : in integer; nbTransitions : in integer; visite : in out tabBoolean; result : in out boolean) is
   begin
      -- si la transition est franchissable pour ce marquage -> retourne vrai
      if (marq.suivant(transition) /= -1)
      then result := true;
         return;
      end if;

      -- sinon, test si la transition est franchissable en franchissant d'autres transitions avant
      for i in 1 .. nbTransitions loop
         if (marq.suivant(i) /= -1)
         then
            if (visite(marq.suivant(i)) = FALSE)
            then
               visite(marq.suivant(i)) := TRUE;
               transitionEstVivante(lMarq, lMarq(marq.suivant(i)), transition, nbTransitions, visite, result);
               if (result = true)
               then return;
               end if;
            end if;
         end if;
      end loop;
   end transitionEstVivante;


   ----------------------------------------------
   -- PROCEDURE EstQuasiVivant
   -- Test si un reseau est quasi vivant
   ----------------------------------------------
   function    estQuasiVivant  (lMarq : in ListMarquage; nbCourant : in integer; nbTransitions : in integer) return boolean is
      visite : tabBoolean;
      result : boolean;
   begin
      -- pour chaque transition
      for i in 1 .. nbTransitions loop
         -- aucun transition n'a ete franchie
         for i in 1 .. nbCourant loop
            visite(i) := FALSE;
         end loop;
         result := FALSE;
         -- test si la transition est vivante
         transitionEstVivante(lMarq, lMarq(1), i, nbTransitions, visite, result);
         if (result = FALSE)
         then
            return false;
         end if;
      end loop;

      return TRUE;
   end estQuasiVivant;


   ----------------------------------------------
   -- PROCEDURE EstVivante
   -- Test si un reseau est vivant
   ----------------------------------------------
   function    estVivant  (lMarq : in ListMarquage; nbCourant : in integer; nbTransitions : in integer) return boolean is
      visite : tabBoolean;
      result : boolean;
   begin
      for t in 1..nbCourant loop --pour chaque marquage
         --pour chaque transition, on regarde si elle est vivante pour le marquage t
         for i in 1 .. nbTransitions loop
            for i in 1 .. nbCourant loop
               visite(i) := FALSE;
            end loop;

            result := FALSE;

            transitionEstVivante(lMarq, lMarq(t), i, nbTransitions, visite, result);

            if (result = FALSE)
            then
               return false;
            end if;
         end loop;
      end loop;
      return true;
   end estVivant;

   ----------------------------------------------
   -- PROCEDURE EstSansBlocage
   -- Test si un reseau est sans blocage
   ----------------------------------------------
   function    estSansBlocage  (lMarq : in ListMarquage; nbCourant : in integer; nbTransitions : in integer) return boolean is
      cpt : integer := 0;
   begin
      -- pour chaque marquage
      for i in 1 .. nbCourant loop
         cpt := 0;
         -- test si le marquage i n'est pas un etat puits
         for j in 1..nbTransitions loop
             if (lMarq(i).suivant(j) /= -1)
            then
               cpt := cpt + 1;
            end if;
         end loop;
         if (cpt = 0)
         then
            return false;
         end if;
      end loop;

      return true;
   end estSansBlocage;


   ----------------------------------------------
   -- PROCEDURE Put
   -- Affiche la liste des marquages accessibles
   ----------------------------------------------
   procedure Put (lMarq : in ListMarquage; nbCourant : in integer) is
   begin
      Text_Io.New_Line;
      Text_Io.Put_Line("  Marquages accessibles :");
      for i in 1..nbCourant loop
         Marquage_Accessible.Put (lMarq (i), i);
      end loop;
   end Put;


end list_marquage_accessible;
